COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb CONJECTURES ABOUT CONTINUOUS FUNCTIONS ON FLAT DOMAINS


	The theory of (Cartwright 1976) and (McCarthy 1977) can be
generalized so as not to give a special role to conditional expressions
which can be regarded as merely one monotonic but non-strict function of
three arguments in flat domains.  (Recall that on flat domains
monotonicity and continuity are the same).  The theory that assures fixed
points and which characterizes functions by the functional equation and
minimization schema is unaltered if we allow additional monotonic
functions as base functions.  The special role of conditional expressions
reduces to the fact that if all the functions occurring in the right side
of a recursive definition are strict, the least fixed point will be the
totally undefined function.

	An immediate question is whether we get anything new by allowing
more monotonic functions and the immediate answer is yes.  Consider the
function ⊗por defined by

	!!a1:  %2por(x,y) = qif x = qb ∧ y = qb qthen qb qelse T%1.

	⊗por may be called "parallel or".  On the one hand it is
monotonic, and on the other hand it cannot be made by composing the
conditional with strict functions.  The reader is invited to ask, "What do
you mean you can't make it with the conditional?  Haven't you just done it
in ({eq a1})"?  Yes, we have, but we used the conditional in a
non-monotonic way, because of the terms %2x = qb%1 and %2y = qb%1.
We can't do it with the monotonic conditional, because anything built up
withh the monotonic conditional has the property that it is strict in the
first variable encountered, and ⊗por isn't strict in either of its
arguments.

	Now we come to the conjecture that all we need is the monotonic
conditional and ⊗por itself.  This conjecture can be formulated in several
ways that are not obviously equivalent.

.item← 0
	#. Consider a function of several arguments built up from
variables and constants including qb using conditional expressions
and equality.  Such a function need not be monotonic but suppose it
is.  The conjecture is that the the function is a composition of
the continuous conditional expression, ⊗por, and the continuous
strict version of equality.

	#. Suppose we have a monotonic function.  We conjecture
that it can be built by composition from the continuous conditional
expression, ⊗por, and various strict functions all of which are
below the original function.


References:

%3Cartwright, Robert %1(1976),  %CA practical formal semantic definition and verification
system for typed LISP%1, Stanford Artificial Intelligence Laboratory technical
report AIM-296, Stanford, California.

%3McCarthy, John%1 (1977)
"Representation of Recursive Programs in
First Order Logic" (to be published). (Draft available as FIRST.NEW[W77,JMC]
at SU-AI on ARPAnet).

	This file is CONJEC[W78,JMC] at SU-AI and this version
was pubbed on {date}.